a, b, c:. imin(a;imin(b;c)) = imin(imin(a;b);c)   

latex

Up	int 2, int 2
Definitions	T, P  Q, P  Q, P & Q, P  Q, True, t  T, x:A. B(x),
Lemmas	true wf, squash wf, imax wf, minus imin, minus mono wrt eq, imin wf, imax assoc